AgdaによるGalois理論のプログラミング
Menu Menu
motivation
5次方程式が代数的に解けないことの復習数学書では省略されてても Agda は許してくれない
計算で示しても、それが証明になっているかどうかは別
証明付きデータ構造を使う
計算と証明が「全部つながってる」
この計算、いったい、何を計算してるの?
それを型で示す
Galois theory : 多項式方程式
(x - α)(x - β)(x - γ) = 0と因数分解されればαβγが解になる。
Galois theory : 解と置換群(対称群)
αβγを入れ替えても良い(Symmetric Group))。これが
(x - α)(x - β) = 0に帰着されるなら、αβ を入れ替えても良い。ならば、αβγ の置換で
αβγ = βαγにならないとおかしい。
Galois theory : 可解群
αβγ = βαγ α⁻¹β⁻¹αβγγ⁻¹ = α⁻¹β⁻¹βαγγ⁻¹ α⁻¹β⁻¹αβ = e (交換子 Commutator)なので、対称群のすべての要素を α⁻¹β⁻¹αβ の形にするのを繰り返して e になれば良い(可解群)。
(もちろん、これは証明になってない。気分的な説明。本当は正規拡大体とか代数的拡大とか)
ここは今回は Agda で証明しません。
あれ? 割と Agda の得意な分野なのでできるはず。やさしくはないだろうけど
Agdaは抽象的な証明が得意
5次方程式が代数的に解けないことの証明
5次の対称群は可解でないことを示せばよい。2,3,4次は可解。教科書だと
これは良い方で、岩波だと練習問題。
数学の本の記述の特徴
理解した後で読むとちゃんと書いてある理解する前には何が書いてあるのかわからない
Agda でちゃんとやろうぜ
Curry Howard 対応に基づく定理証明支援系
依存型を持つ純関数型言語
依存型とは、型を値に持つ変数
命題そのものは Set という型を持つ
構文的には Haskell とほぼ同じ。Coq と違い、何もしてくれない。全部、自分で証明を書く。(いさぎよい)
Agda : lambda
A → B の証明
→intro : {A B : Set } → A → B → ( A → B )
→intro _ b = λ x → b
→elim : {A B : Set } → A → ( A → B ) → B
→elim a f = f a
引数の値は、型の証明
入力は∀が付いていると考える(∃はあとで)
Agda : record
A ∧ B の証明
record _∧_ (A B : Set) : Set where
field
proj1 : A
proj2 : B
∧elim : {A B : Set} → ( A ∧ B ) → A
∧elim a∧b = proj1 a∧b
∧intro : {A B : Set} → A → B → ( A ∧ B )
∧intro a b = record { proj1 = a ; proj2 = b }
Agda : data
A ∨ B の証明
data _∨_ (A B : Set) : Set where
case1 : A → A ∨ B
case2 : B → A ∨ B
∨intro : {A B : Set} → A → ( A ∨ B )
∨intro a = case1
∨elim : {A B : Set} → ( A ∨ A ) → A
∨elim (case1 a) = a
∨elim (case2 a) = a
Agda : negation
data ⊥ : Set where
constructor のないデータ構造(偽
⊥-elim : {A : Set } -> ⊥ -> A
⊥-elim ()
起きない入力は () 。λ () とも書ける
data ⊤ : Set where
tt : ⊤
要素が一つしかない型(真
Agda : unification
data _≡_ {A : Set } : A → A → Set where
refl : {x : A} → x ≡ x
≡intro : {A : Set} {x : A } → x ≡ x
≡intro = refl
≡elim : {A : Set} {x y : A } → x ≡ y → y ≡ x
≡elim refl = refl
項(正規化された)として等しい。変数はどうするの? 十分に instanciation されない場合は黄色くなる。
その他、細かい問題が... internal parametricity... inspect...
でも、これで全部。さぁ、Agda を書こう。
Galois theory i nAgda : Commutator
[_,_] : Carrier → Carrier → Carrier
[ g , h ] = g ⁻¹ ∙ h ⁻¹ ∙ g ∙ h
こんな風に数学の教科書通りに Unicode を使って書けるところが Agda の良いところ
data Commutator (P : Carrier → Set ) : (f : Carrier) → Set where
comm : {g h : Carrier} → P g → P h → Commutator P [ g , h ]
ccong : {f g : Carrier} → f ≈ g → Commutator P f → Commutator P g
deriving : ( i : ℕ ) → Carrier → Set
deriving 0 x = ⊤
deriving (suc i) x = Commutator (deriving i) x
Set を返してるのはなに? Set は何かの命題、 つまり真偽として扱って良い。したがって
P : Carrier → Set
これは Carrier の部分集合を指定する命題となる。 (Carrier は群の要素の型)
交換子 Commutator p は述語 f p で限定された p : Carrier が [ g , h ] という形で生成されることを示している。
deriving i は、Carrier の部分集合で、Commutator を再帰的に繰り返して得られたもの
Galois theory in Agda : Solvable
record solvable : Set (Level.suc n ⊔ m) where
field
dervied-length : ℕ
end : (x : Carrier ) → deriving dervied-length x → x ≈ ε
存在∃は record で書く。ある dervied-length : ℕ があって、その回数のderive の繰り返しで x ≈ ε になる
この record を構成できれば、その群は可解ということになる。これで問題は定義できた
Galois theory in Agda : Symmetric group
対称群の要素は置換だが、Agdaの標準ライブラリだと有限な数のBijectionとして定義される
Permutation p p定義は複雑だが二つの写像 _⟨$⟩ˡ_ _⟨$⟩ʳ_ と y ⟨$⟩ˡ (y ⟨$⟩ʳ x) ≡ x と y ⟨$⟩ʳ (y ⟨$⟩ˡ x) ≡ x からなる record
残念ながら扱いにくい。同等性とか。単純に x ≡ y を証明できない(Agdaの制約 1)
しかし群であることを示すのは簡単
Permutation : Data.Fin
有限な数
data Fin : ℕ → Set where
zero : {n : ℕ} → Fin (suc n)
suc : {n : ℕ} (i : Fin n) → Fin (suc n)
x : Fin 3 のように使う
Fin 0 の値は存在しない
_⟨$⟩ˡ_ : Fin p → Fin p
Permutation : List
置換は List ℕ で表されるので、それで良いのだが、List ℕ が全部置換になるわけではない
そこで減少列 FL とその大小関係を定義する
data FL : (n : ℕ )→ Set where
f0 : FL 0
_::_ : { n : ℕ } → Fin (suc n ) → FL n → FL (suc n)
data _f<_ : {n : ℕ } (x : FL n ) (y : FL n) → Set where
f<n : {m : ℕ } {xn yn : Fin (suc m) } {xt yt : FL m} → xn Data.Fin.< yn → (xn :: xt) f< ( yn :: yt )
f<t : {m : ℕ } {xn : Fin (suc m) } {xt yt : FL m} → xt f< yt → (xn :: xt) f< ( xn :: yt )
すると、これは置換と 1 to 1 になる。しかし 1 to 1 の証明は煩雑。しかし、簡単な方法があるかも。
煩雑でも証明できてしまえば問題ないので、簡単にする motivation はあまりでない。
でも簡単にしておくと、次に使えるかも。
Proofs : 2
これで道具立てはそろったので証明に行くまず、二次対称群から
sym2lem0 : ( g h : Permutation 2 2 ) → (q : Fin 2) → ([ g , h ] ⟨$⟩ʳ q) ≡ (pid ⟨$⟩ʳ q)
sym2lem0 = ?
solved : (x : Permutation 2 2) → Commutator (λ x₁ → Lift (Level.suc Level.zero) ⊤) x → x =p= pid
solved x (comm {g} {h} _ _) = record { peq = sym2lem0 g h }
となるのだが、g と h が何かわからないので FL 2 に変換する
FL 2 は
zero :: (zero :: f0)というものなので、これが pid つまり恒等置換であることは証明してあるのだが
FL-inject : {n : ℕ } → {g h : Permutation n n } → perm→FL g ≡ perm→FL h → g =p= h
を証明して使う。ところが、
pleq : {n : ℕ} → (x y : Permutation n n ) → plist0 x ≡ plist0 y → x =p= y
を使うと
p0 : FL→perm ((# 0) :: ((# 0 ) :: f0)) =p= pid p0 = pleq _ _ reflとできる。Injection は圏論でいう Equalizaer で写像した先で等しいなら手元でも等しいという性質
Proofs : 3
2でこれなので 3 は絶望的に煩雑になるたぶん、ガロアはそれを手で計算したはず
Proofs : 5
5は、solvable が存在しない、つまり否定を示せばよいsolvable から矛盾 counter-example を作る
¬sym5solvable : ¬ ( solvable (Symmetric 5) )
¬sym5solvable sol = counter-example (end5 (abc 0<3 0<4 ) (dervie-any-3rot0 (dervied-length sol) 0<3 0<4 ) ) where
3次の対称群を含むことを示せばよいのだが、それが dervie-any-3rot0 実は dervie-any-3rot0 と dervie-any-3rot1 がいる
教科書だと「要素三つがとれるよね」と書いてあるが、Agda だと具体的に取ってくる必要がある。「あとは同じだよね」と書いてあっても、それを示す必要がある。
もっと簡単にできるでしょ
derving は簡単に計算できるので、それで証明した方が良いんじゃないの?確かにその通り
計算は簡単だが、それを証明にするにはどうすれば良いの?
すべての交換子の組み合せを計算している
を証明すればよい
つまり sort された List に、全部の要素が含まれている (どんな要素でも入っている) any ことを Agda で書く
それには Fresh List というのを使う
Fresh List
(A : Set )と (R : A → A → Set) に対して
data List# : Set
[] : List#
cons : (a : A) (as : List#) → fresh a as → List#
という List を定義する
fresh : (a : A) (as : List#) → Set
fresh a [] = ⊤
fresh a (cons x xs _) = R a ∧ fresh a xs
普通の∷ (cons)の代わりに _∷#_ を使う
infixr 5 _∷#_
pattern _∷#_ x xs = cons x xs _
これも Set を値にしている。Fresh List の最後とそうでないもので fresh の中身が違う
List の要素毎に、fresh が存在するので、結構でかいものになる(O(2^n))。
FList : (n : ℕ ) → Set
FList n = List# (FL n) ⌊ _f<?_ ⌋
fr1 : FList 3
fr1 =
((# 0) :: ((# 0) :: ((# 0 ) :: f0))) ∷#
((# 0) :: ((# 1) :: ((# 0 ) :: f0))) ∷#
((# 1) :: ((# 0) :: ((# 0 ) :: f0))) ∷#
((# 2) :: ((# 0) :: ((# 0 ) :: f0))) ∷#
((# 2) :: ((# 1) :: ((# 0 ) :: f0))) ∷#
[]
と定義できる。これで FList 3 が sort されていることが「証明されている」。⌊ _f<?_ ⌋ が不思議だが...
Fresh List : Any
data Any : List# A R → Set where
here : ∀ {x xs pr} → P x → Any (cons x xs pr)
there : ∀ {x xs pr} → Any xs → Any (cons x xs pr)
ここにあったら here、先にあるなら there
Any (x ≡_) (FLinsert x xs)
という形で使う。
x ≡_
は
λ y → x ≡ y
のこと。 _≡_ x と書いても良い。
ちなみに、
x _≡
は
λ y → y ≡ x
なので意味が異なる (≡は対称なので結局は同じなのだが、Agda の推論はそこまでカバーしない)
これで三日くらい悩みました
Fresh List : Insert
普通の insert と変わらないけど、fresh を作る必要がある
FLinsert : {n : ℕ } → FL n → FList n → FList n
FLinsert {zero} f0 y = f0 ∷# []
FLinsert {suc n} x [] = x ∷# []
FLinsert {suc n} x (cons a y x₁) with FLcmp x a
... | tri≈ ¬a b ¬c = cons a y x₁
... | tri< lt ¬b ¬c = cons x ( cons a y x₁) ( Level.lift (fromWitness lt ) , ttf lt y x₁)
FLinsert {suc n} x (cons a [] x₁) | tri> ¬a ¬b lt = cons a ( x ∷# [] ) ( Level.lift (fromWitness lt) , Level.lift tt )
FLinsert {suc n} x (cons a y yr) | tri> ¬a ¬b a<x = cons a (FLinsert x y) (FLfresh a x y a<x yr )
Fresh List : Property on Insert / Cons
x∈FLins : {n : ℕ} → (x : FL n ) → (xs : FList n) → Any (x ≡_) (FLinsert x xs)
nextAny : {n : ℕ} → {x h : FL n } → {L : FList n} → {hr : fresh (FL n) ⌊ _f<?_ ⌋ h L } → Any (x ≡_) L → Any (x ≡_) (cons h L hr )
insAny : {n : ℕ} → {x h : FL n } → (xs : FList n) → Any (x ≡_) xs → Any (x ≡_) (FLinsert h xs)
あたりがあると便利
Fresh List : Any on Pair
Commutator (それを作っていたのだった) は任意の pair なので
record AnyComm {n m l : ℕ} (P : FList n) (Q : FList m) (fpq : (p : FL n) (q : FL m) → FL l) : Set where
field
commList : FList l
commAny : (p : FL n) (q : FL m)
→ Any ( p ≡_ ) P → Any ( q ≡_ ) Q
→ Any (fpq p q ≡_) commList
つまり二つの FList から、組を全部生成する必要がある。(fpq は ∧ の方が良かったか?)
(p,q) (p,qn) .... (p,q0)
pn,q
: AnyComm FL0 FL0 P Q
p0,q
こんな風に再帰で作れる(やさしくない
Fresh List : Solved using Fresh List
まず全部の FL が入ってる FList
record AnyFL (n : ℕ) : Set where
field
allFL : FList n
anyP : (x : FL n) → Any (x ≡_ ) allFL
これは AnyComm から作れる (やさしくない
次に Commutator
CommFListN : ℕ → FList n
CommFListN zero = allFL (anyFL n)
CommFListN (suc i ) = commList (anyComm ( CommFListN i ) ( CommFListN i ) (λ p q → perm→FL [ FL→perm p , FL→perm q ] ))
そして、Commutator がちゃんと全部入っていることを示す(やさしい
CommStage→ : (i : ℕ) → (x : Permutation n n ) → deriving i x → Any (perm→FL x ≡_) (CommFListN i)
すると
CommSolved : (x : Permutation n n) → (y : FList n) → y ≡ FL0 ∷# [] → (FL→perm (FL0 {n}) =p= pid ) → Any (perm→FL x ≡_) y → x =p= pid
という形で可解を定義できる。
Proofs : 2
以下のように極めて簡単になった(やった!
stage2FList : CommFListN 2 1 ≡ cons (zero :: zero :: f0) [] (Level.lift tt)
stage2FList = refl
solved1 : (x : Permutation 2 2) → deriving 1 x → x =p= pid
solved1 x dr = CommSolved 2 x ( CommFListN 2 1 ) stage2FList p0id solved0 where
solved0 : Any (perm→FL x ≡_) ( CommFListN 2 1 )
solved0 = CommStage→ 2 1 x dr
このまま 3, 4を証明可能
Proofs : 5
e 以外を含む stage 3 が stage 4 と同じことを示すだけで可解でないことを示せるしかし5を計算すると停まらない(きっと停まるが遅すぎる
メモリは食わない (FList 5 自体は計算できて、それで抑えられる)
単に計算が遅い
時間
agda sym3.agda 258.01s user 2.95s system 98% cpu 4:23.68 total
agda sym3n.agda 9.18s user 0.45s system 95% cpu 10.089 total
agda sym2n.agda 9.09s user 0.35s system 99% cpu 9.454 total
agda sym2.agda 9.34s user 0.50s system 94% cpu 10.448 total
agda sym4.agda 9.38s user 0.37s system 99% cpu 9.784 total
agda sym5.agda 9.04s user 0.34s system 99% cpu 9.427 total
しかし、Agda には compiler が!
コンパイルすれば計算可能
./sym5n 0.00s user 0.01s system 37% cpu 0.044 total
ただし、それは証明には接続できない
型検査時に compile して計算する機能はない
これが証明に接続されると、5次が可解でないことはわかるが、その理由はわからない。不可解な証明だということになる。
Analysis : overhead of proof carrying data structure
Fin, Commutator, FL, Fresh , Any, FList は、すべて証明付きデータ構造証明は実行時ではなく型検査時に行われるので実行時のオーバヘッドは理論的にはない
Any や fresh は実行されない型しか計算しないコードになる
しかし、Fresh は Product を含んでいるので実際に heapを食うのでオーバーヘッドがあるように見える
ところが、それは使われないので実行時には明示的に触らない限り生成されない(遅延評価
なので、普通に高速に計算される
Analysis connection of computation and type
普通は何を計算したのかは計算機は知らないまして作った人以外はさっぱりわからない
しかし、証明付きデータならば、そこに何を計算したのかが書いてある
ただ
プログラミングは、めっちゃ面倒
でも、それができるならプログラミングの信頼性は上がる
しかし、それでも完全に正しいとは...
Appendix : ZF fix
証明があっても正しいとは限らない去年のZFには間違いがあって
record OD : Set (suc n ) where
field
def : (x : Ordinal ) → Set n
OD ⇔ Ordinal を要求すると矛盾になる
¬OD-order : ( & : OD → Ordinal ) → ( * : Ordinal → OD ) → ( { x y : OD } → def y ( & x ) → & x o< & y) → ⊥
¬OD-order & * c<→o< = osuc-< <-osuc (c<→o< {Ords} OneObj )
なので最大値を付けてやると良い
record HOD : Set (suc n) where
field
od : OD
odmax : Ordinal
<odmax : {y : Ordinal} → def od y → y o< odmax
つまり証明が合ってても仮定が間違ってたらダメ
これは (集合論の用語での) Set と Class の区別になっている。つまり OD が Class で、最大値があれば集合になる。
Appendix : Topology
今年は
record Toplogy ( L : HOD ) : Set (suc n) where
field
OS : HOD
OS⊆PL : OS ⊆ Power L
o∪ : { P : HOD } → P ⊆ OS → OS ∋ Union P
o∩ : { p q : HOD } → OS ∋ p → OS ∋ q → OS ∋ (p ∩ q)
やっても良いかも。 Tychonovの定理の証明とか(やさしくなさそう
あるいは ZF の cohen model とか
record Filter ( L : HOD ) : Set (suc n) where
field
filter : HOD
f⊆PL : filter ⊆ Power L
filter1 : { p q : HOD } → q ⊆ L → filter ∋ p → p ⊆ q → filter ∋ q
filter2 : { p q : HOD } → filter ∋ p → filter ∋ q → filter ∋ (p ∩ q)
Topology と Filter は似てることがわかる
Permutation : 等号
record _=p=_ {p : ℕ } ( x y : Permutation p p ) : Set where
field
peq : ( q : Fin p ) → x ⟨$⟩ʳ q ≡ y ⟨$⟩ʳ q
を統合して使う
x ≡ y → x =p y
は言えるが
x =p y → x ≡ y
は仮定するしかない。(Functional Extentionality)
Permutation : Data.Fin と Data.Nat
suc と zero が自然数と重なっていて扱いを気をつける必要がある
data ℕ : Set where
zero : ℕ
suc : ℕ → ℕ
x ∧ x < n で不等号を持ち歩く方法でも良いのだが...
x < n も
data _≤_ : Rel ℕ 0ℓ where
z≤n : ∀ {n} → zero ≤ n
s≤s : ∀ {m n} (m≤n : m ≤ n) → suc m ≤ suc n
と再帰的データ構造なので二重に持ち歩くことになるので美しくない
Permutation : FL と Permutation の対応の証明
Permutation の combinator 表現を使う
pprep 先頭に一つ置換を増やす
pswap 先頭の二つを入れ替える
これだけで任意の置換を構成できる
これから pins という任意の置換に任意の位置に 0(の位置の要素) を入れる関数を作る
そして、pins の逆を
pshrink 置換を一つ減らす
を作って構成する
極めて煩雑な証明になる
Fresh List : witness
⌊ _f<?_ ⌋ は witness と呼ばれるもので、
data Dec : {R : FL → FL → Set} : Set where
yes : R → Dec R
no : ¬ R → Dec R
x f<? y with FLcmp x y
... | tri< a ¬b ¬c = yes a
... | tri≈ ¬a refl ¬c = no ( ¬a )
... | tri> ¬a ¬b c = no ( ¬a )
sym5
abc が反例。これが常に残ることを示す
counter-example : ¬ (abc 0<3 0<4 =p= pid )
counter-example eq with ←pleq _ _ eq
... | ()
二つ余地を確保する
ins2 : {i j : ℕ } → Permutation 3 3 → (i ≤ 3 ) → ( j ≤ 4 ) → Permutation 5 5
ins2 abc i<3 j<4 = (save2 i<3 j<4 ∘ₚ (pprep (pprep abc))) ∘ₚ flip (save2 i<3 j<4 )
abc と dba を作る
abc : {i j : ℕ } → (i ≤ 3 ) → ( j ≤ 4 ) → Permutation 5 5
abc i<3 j<4 = ins2 3rot i<3 j<4
dba : {i j : ℕ } → (i ≤ 3 ) → ( j ≤ 4 ) → Permutation 5 5
dba i<3 j<4 = ins2 (3rot ∘ₚ 3rot) i<3 j<4
abc が derive されることを示す
dervie-any-3rot0 : (n : ℕ ) → {i j : ℕ } → (i<3 : i ≤ 3 ) → (j<4 : j ≤ 4 )
→ deriving n (abc i<3 j<4 )
dervie-any-3rot0 0 i<3 j<4 = lift tt
dervie-any-3rot0 (suc i) i<3 j<4 = ccong {deriving i} (psym ceq) (commd dba0 aec0 df dg )where
commd : {n : ℕ } → (f g : Permutation 5 5)
→ deriving n f
→ deriving n g
→ Commutator (deriving n) [ f , g ]
commd {n} f g df dg = comm {deriving n} {f} {g} df dg
df と dg が前に derive されたもの
df = dervie-any-3rot1 i (fin≤n {3} (dba0<3 tc)) (fin≤n {4} (dba1<4 tc))
dg = dervie-any-3rot1 i (fin≤n {3} (aec0<3 tc)) (fin≤n {4} (aec1<4 tc))
それは、再帰的に作れるのだが種(dbaとaec)を二つ計算する必要がある
それは右回転と左回転があって、 dervie-any-3rot0 と dervie-any-3rot1 で交互に作られる
そのつくり方だが...
tc = triple i<3 j<4
dba0 = dba (fin≤n {3} (dba0<3 tc)) (fin≤n {4} (dba1<4 tc))
aec0 = dba (fin≤n {3} (aec0<3 tc)) (fin≤n {4} (aec1<4 tc))
ceq : abc i<3 j<4 =p= [ dba0 , aec0 ]
ceq = record { peq = peq (abc= tc) }
dba と aec を作るのだが
record Triple {i j : ℕ } (i<3 : i ≤ 3) (j<4 : j ≤ 4) (rot : Permutation 3 3) : Set where
field
dba0<3 : Fin 4
dba1<4 : Fin 5
aec0<3 : Fin 4
aec1<4 : Fin 5
abc= : ins2 rot i<3 j<4 =p= [ ins2 (rot ∘ₚ rot) (fin≤n {3} dba0<3) (fin≤n {4} dba1<4) , ins2 (rot ∘ₚ rot) (fin≤n {3} aec0<3) (fin≤n {4} aec1<4) ]
open Triple
triple : {i j : ℕ } → (i<3 : i ≤ 3) (j<4 : j ≤ 4) → Triple i<3 j<4 3rot
triple z≤n z≤n = record { dba0<3 = # 0 ; dba1<4 = # 4 ; aec0<3 = # 2 ; aec1<4 = # 0 ; abc= = pleq _ _ refl }
triple z≤n (s≤s z≤n) = record { dba0<3 = # 0 ; dba1<4 = # 4 ; aec0<3 = # 2 ; aec1<4 = # 0 ; abc= = pleq _ _ refl }
....
と自分でうまく2つの余地を選択する必要がある
もちろん、計算することは可能だが...